es:ES, A, triggerV:Type, l:IdLnk, tg:Id, knd:Knd, ds:x:Id fp Type,
cond:(State(ds)triggerV(A + Top)).
(e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (e:E.
 (loc(e) = source(l)  Id)
  (kind(e) = knd)
  ((valtype(e) r triggerV) & (state@loc(e) r State(ds))))
 (p:(e:E.
 (p:(Dec((isrcv(e)) & lnk(e) = l & loc(sender(e)) = source(l)  Id & kind(sender(e)) = knd)).
 knd(v:triggerV) sends on l [tg:A, p.let s,v = p in cond(s,v) <state, v>]?[]
  glues(es;
  glues(A;
  glues((e.sender(e));
  glues((e.outl(cond((state when e),val(e))));
  glues(es-trigger(es;source(l);knd;ds;cond);
  glues((es-in-port(es;l;tg)|p))) 

latex

Definitions

ES, t  T, f(a), EState(T), Id, , x:AB(x), x:A. B(x), pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, Type, suptype(S; T), first(e), b, A, loc(e), <a, b>, s = t, P  Q, constant_function(f;A;B), IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x:A  B(x), P & Q, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(E; pred?; info), EqDecider(T), Atom$n, (x  l), {x:A| B(x)} , State(ds), a:A fp B(a), valtype(e), rcv(l,tg), kind(e), E, state@i, source(l), loc(e), sender(e), lnk(e), t.1, if b then t else f fi , ff, tt, locl(a), let x,y = A in B(x;y), False, True, case b of inl(x) => s(x) | inr(y) => t(y), , A c B, Dec(P), isrcv(e), x.A(x), k(v:B) sends on l [tg:T, f <state, v>]?[], es-trigger(es;i;knd;ds;f), glues(es; B; g; f; Ia; Ib), a = b, P  Q, P  Q, {T}, a = b, Q ==f== P, Q = f== P, e loc e' , f is Q-R-pre-preserving on P, Inj(A;B;f), acttype(e), rcvtype(e), es-in-port(es;l;tg), AbsInterface(A), (I|p), E(X), e  X, X(e), outl(x), {I}, x:A. B(x), g glues Ia:Qa f Ib:Rb, P  Q, x(s), (e < e'), e c e', inr x , inl x , T, can-apply(f;x), val(e), (state when e), isl(x), SQType(T), s ~ t, (e <loc e'), vartype(i;x), f(x)?z, IdDeq, @i discrete ds, b, do-apply(f;x), tag(e)

Lemmas

es-rcv-kind, member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not functionality wrt iff, outl wf, es-state-subtype2, es-dds wf, es-interface-val-restrict, can-apply wf, es-state-subtype, fpf-cap wf, id-deq wf, es-vartype wf, sender-le-pre-preserving, es-is-interface-restrict2, es-causle-le, es-locl wf, es-le wf, es-isrcv-loc, IdLnk sq, Knd sq, squash wf, es-kind-rcv, es-is-interface-in-port, isl wf, es-state-when wf, es-val wf, es-is-interface-trigger, subtype rel dep function, subtype rel sum, subtype rel function, es-sender-causl, es-causle weakening, es-trigger wf, es-is-interface-restrict, decidable assert, es-is-interface wf, es-E-interface wf, es-interface-restrict wf, es-in-port wf, es-rcvtype wf, es-acttype wf, assert-eq-id, eq id wf, all functionality wrt iff, implies functionality wrt iff, assert-eq-knd, eq knd wf, subtype rel wf, conditional-send-p wf, es-isrcv wf, decidable wf, true wf, false wf, locl wf, btrue wf, bfalse wf, es-lnk wf, es-sender wf, es-loc wf, lsrc wf, es-state wf, es-E wf, es-kind wf, rcv wf, es-valtype wf, decl-state wf, l member wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf